package adder;

import java.util.ArrayList;

import JaCoP.constraints.And;
import JaCoP.constraints.Constraint;
import JaCoP.constraints.Or;
import JaCoP.constraints.Reified;
import JaCoP.constraints.XeqY;
import JaCoP.constraints.XneqY;
import JaCoP.core.IntVar;
import JaCoP.core.Store;
import JaCoP.search.DepthFirstSearch;
import JaCoP.search.IndomainMin;
import JaCoP.search.InputOrderSelect;
import JaCoP.search.Search;
import JaCoP.search.SelectChoicePoint;

public class Adder {
	int in1 = 1;
	int in2 = 1;
	int c = 0;

	public Adder() {
		Store store = new Store();
		ArrayList<IntVar> vars = new ArrayList<IntVar>();
		IntVar in1 = new IntVar(store, "IN1", 0, 1);
		IntVar in2 = new IntVar(store, "IN2", 0, 1);
		IntVar c = new IntVar(store, "C", 0, 1);
		IntVar x1 = new IntVar(store, "X1", 0, 1);
		IntVar a1 = new IntVar(store, "A1", 0, 1);
		IntVar a2 = new IntVar(store, "A2", 0, 1);
		;
		IntVar s = new IntVar(store, "S", 0, 1);
		IntVar carry = new IntVar(store, "CARRY", 0, 1);
		IntVar one = new IntVar(store, 1, 1);

		vars.add(in1);
		vars.add(in2);
		vars.add(c);
		vars.add(x1);
		vars.add(a1);
		vars.add(a2);
		vars.add(s);
		vars.add(carry);
		vars.add(one);

		store.impose(new Reified(
				new And(new XeqY(in1, one), new XeqY(in2, one)), a1));
		store.impose(new Reified(
				new Or(new XeqY(in1, one), new XeqY(in2, one)), x1));
		store.impose(new Reified(new Or(new XeqY(x1, one), new XeqY(c, one)), s));
		store.impose(new Reified(new And(new XeqY(x1, one), new XeqY(c, one)),
				a2));
		store.impose(new Reified(new And(new XeqY(a1, one), new XeqY(a2, one)),
				carry));

		IntVar[] v = new IntVar[vars.size()];
		vars.toArray(v);

		Search<IntVar> search = new DepthFirstSearch<IntVar>();
		SelectChoicePoint<IntVar> select = new InputOrderSelect<IntVar>(store,
				v, new IndomainMin<IntVar>());

		search.getSolutionListener().searchAll(true);
		search.getSolutionListener().recordSolutions(true);

		// for (int i = 1; i <= search.getSolutionListener().solutionsNo(); i++)
		// {
		// System.out.print("Solution " + i + ": ");
		// for (int j = 0; j < search.getSolution(i).length; j++)
		// System.out.print(search.getSolution(i)[j]);
		// System.out.println();
		// }

		//
		boolean result = search.labeling(store, select);

		if (result)
			System.out.println("Solution: " + v[0] + ", " + v[1] + ", " + v[2]
					+ " gives " + v[6] + ", " + v[7]);
		else
			System.out.println("*** No");

		System.out.println("------------------");
		System.out.println("in1,in2,c,-,-,-,sum,carry,-");
		search.getSolutionListener().printAllSolutions();
	}
}
